$\forall$${\it es}$:event\_system\{i:l\}. es\_init(${\it es}$) $\in$ $i$:Id$\rightarrow$es\_state(${\it es}$; $i$)